Fix let inference (attempts to fix #72 and #82). #89
Conversation
|
I'll take a look at this. |
|
I am certainly no expert, so take this comment with a grain of salt, but I took a glance at this, and it looks right to me. I think it might be possible to implement it more nicely, though, by keeping the use of |
|
I know this is several years late, but there is indeed a better solution, which I found while trying to build my own compiler as a learning exercise, using the code here as a starting point. in particular, the code infer expr = case expr of
...
Let x e1 e2 -> do
env <- ask
t1 <- infer e1
let sc = generalize env t1
...should be infer expr = case expr of -- < I would also use LambdaCase here
...
Let x e1 e2 -> do
env <- ask
(t0, constraints) <- listen $ infer e1
subst <- liftEither $ runSolve constraints
let t1 = apply subst t0
sc = generalize env t1
...The issue, as I'm sure is well known, is that we generate constraints for the type variable in the scheme bound to This can be fixed simply by listening to the constraint generation while inferring the RHS of the binding, solving the constraints, and applying the substitution to to the type of The algorithm referenced in #82 warns of a caveat with generalization, but the existing logic seems to already handle it; the given example: (\f x -> let g = f in g 0) (\x -> if x then True else False) Truefails the type checker. |
See <sdiehl/write-you-a-haskell#89>. The problem could be manifested by trying to type check: (let ((f (λ f (+ f 1)))) (f "foo")) which would pass type checking and fail at runtime. The cause was that when we did t1 <- infer e1 we would get a type variable along with some constraints on it. Like 'TVar e where e ~ Float'. But then we generalized e to `forall e. e` without knowing it unified with Float, and that's totally different.
as documented in pr#89 sdiehl/write-you-a-haskell#89 the original approach of the tutorial had an issue with `let` inference. the PR implemented a new approach which resolves the issue. this commit adapts the code to take that approach.
* add types module * beginnings of type inference! * add `env` module for typing environment sdiehl has a module which presents a subset of (the wrapped) `Data.Map` API. this is my take on that. it doesn't seems strictly necessary - we can probably just use `HashMap` directly, and perhaps it would be nicer to just do that, because it implements so many handy traits. I thought this would teach me a bit about API design and also about Rust trait stuff. we can rewrite later if we feel it's not worth its maintenance cost. * more on `infer` finish implementing the analogue of `Substitutable`. still seems like this approach is pretty good. I am getting schooled on Rust a bit which is fun. * cargo fmt this was long overdue because I was working on my Mac and it doesn't have `rustfmt` through the nix install for some reason... * eschew (zero cost) indirection: turn `Subst` into a type synonym seems cleaner - we don't get much from the newtype. * cargo fmt * wip: start on infer * wip 2: more `infer`, before realizing we need a diff approach pr#89 on the repo demonstrates that inference was broken. the new approach should work, which is excellent. * pivot: return `Vec<Constraint>` from `infer` as documented in pr#89 sdiehl/write-you-a-haskell#89 the original approach of the tutorial had an issue with `let` inference. the PR implemented a new approach which resolves the issue. this commit adapts the code to take that approach. * flesh out the body of `infer` for all match cases seems to be going smoothly ⛵ * implement `generalize` * implement most of the solver we are now only missing `unify_many`. * implement `unify_many` * finish type inference?? I have now implemented all the functions of `poly`'s `Infer` module. * example of inference - it fails to propagate constraints * rename `Decl` to `Defn` (lisp/scheme style) & define a parser for it had to lift out a bunch of common sub-parsers. turns out the type sigs are verbose but almost entirely the same from one to the next - only the arguments and return type really differ. * make a repl which parses & typechecks `Expr`s * setup for demo asciinema * fix bug in `App` type inferece I forgot to perform the substitution from the first unification. d'oh 🤦♂️ * repl: pretty print the scheme * fix import in test broken by adding `util::pretty` module.
Attempts to fix issues #72 and #82 regarding let polymorphism. Inference works correctly for the functions provided in them and they have been added to the test.ml file. Big thanks to @Azure-Vani for the pointer to his / her implementation as well as providing the algorithm described in TAPL.
For this fix, I had to radically change the
inferfunction's interface, and alter the Infer monad to being a simpleState+Reader+Exceptinstead ofRWS(theWriterpart was not being used). This might not be good for readability, but it's the solution I could come up with.Additionally, this is going to need to be reflected in the text, but I'm not confident enough to submit changes to it.